lectures.alex.balgavy.eu

Lecture notes from university.
git clone git://git.alex.balgavy.eu/lectures.alex.balgavy.eu.git
Log | Files | Refs | Submodules

Famous lambda calculus terms.md (435B)

      1 +++
      2 title = "Famous lambda calculus terms"
      3 +++
      4 
      5 # Famous lambda calculus terms
      6 You probably need to memorize these.
      7 - I = 𝜆x.x
      8 - K = 𝜆x.𝜆y.x
      9 - S = 𝜆x.𝜆y.𝜆z.xz(yz)
     10 - Ω = (𝜆x.xx)(𝜆x.xx) — not strongly normalising
     11 
     12 All are closed (no free variables). All are abstractions.
     13 
     14 S, K, and I are terms in the SKI combinator calculus (combinatory logic, 'CL'). CL is undecidable, because you can't derive E ⊢ s = t.